Employing Theory Formation to Guide Proof Planning
Identifieur interne : 000C09 ( Main/Exploration ); précédent : 000C08; suivant : 000C10Employing Theory Formation to Guide Proof Planning
Auteurs : Andreas Meier [Allemagne] ; Volker Sorge [Royaume-Uni] ; Simon Colton [Royaume-Uni]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2002.
English descriptors
- Teeft :
- Algebra, Atp, Automatic concept formation, Basic construction element, Binary operation, Cardinality, Case split, Colton, Computer algebra, Computer algebra system, Computer algebra system maple, Computer science, Concept formation steps, Congruence class, Congruence classes, Control rule, Control rules, Deduction volume, Discriminant, Discriminants, Equational reasoning, Equational reasoning strategy, Example construction, Exhaustive case analysis, External systems, Formal proof, Guide proof planning, Idempotent element, Inductive logic programming, International conference, Invariant property, Isomorphic, Isomorphism, Magma, Mathematical domain, Meier, Method calltrampm, Model generation, Model generator, More detail, Multi, Multiplication table, Multiplication tables, Nding discriminants, Open goal, Other hand, Other structure, Overall proof, Pages morgan kaufmann, Pages springer verlag, Planner, Planning process, Possible functions, Possible properties, Problem domain, Production rule, Production rules, Proof assumptions, Proof attempt, Proof plan, Proof planner, Proof planner multi, Proof planning, Proof plans, Proof procedure, Proof steps, Proof technique, Proof techniques, Provers, Quasigroups, Residue class, Residue class domain, Residue class sets, Residue class structure, Residue class structures, Residue classes, Right identity, Search space, Set1, Set2, Single element, Sorge, Springer verlag, Subsequent proof planning process, Suitable concepts, Suitable discriminant, Theorem provers, Theory formation, Theory formation system, Tramp.
Abstract
Abstract: The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.
Url:
DOI: 10.1007/3-540-45470-5_25
Affiliations:
- Allemagne, Royaume-Uni
- Angleterre, Midlands de l'Ouest, Écosse
- Birmingham, Édimbourg
- Université d'Édimbourg, Université de Birmingham
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001A96
- to stream Istex, to step Curation: 001969
- to stream Istex, to step Checkpoint: 000A01
- to stream Main, to step Merge: 000C10
- to stream Main, to step Curation: 000C09
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Employing Theory Formation to Guide Proof Planning</title><author><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name></author><author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name></author><author><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FFD345C780A55424D028DF36D3FA774C524D5F53</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45470-5_25</idno><idno type="url">https://api.istex.fr/document/FFD345C780A55424D028DF36D3FA774C524D5F53/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001A96</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001A96</idno><idno type="wicri:Area/Istex/Curation">001969</idno><idno type="wicri:Area/Istex/Checkpoint">000A01</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000A01</idno><idno type="wicri:doubleKey">0302-9743:2002:Meier A:employing:theory:formation</idno><idno type="wicri:Area/Main/Merge">000C10</idno><idno type="wicri:Area/Main/Curation">000C09</idno><idno type="wicri:Area/Main/Exploration">000C09</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Employing Theory Formation to Guide Proof Planning</title><author><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name><affiliation wicri:level="1"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Fachbereich Informatik, Universität des Saarlandes</wicri:regionArea><wicri:noRegion>Universität des Saarlandes</wicri:noRegion><wicri:noRegion>Universität des Saarlandes</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name><affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, University of Birmingham</wicri:regionArea><placeName><settlement type="city">Birmingham</settlement><region type="country">Angleterre</region><region type="région" nuts="1">Midlands de l'Ouest</region></placeName><orgName type="university">Université de Birmingham</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author><author><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name><affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>Division of Informatics, University of Edinburgh</wicri:regionArea><placeName><settlement type="city">Édimbourg</settlement><region type="country">Écosse</region></placeName><orgName type="university">Université d'Édimbourg</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2002</date></imprint><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Algebra</term><term>Atp</term><term>Automatic concept formation</term><term>Basic construction element</term><term>Binary operation</term><term>Cardinality</term><term>Case split</term><term>Colton</term><term>Computer algebra</term><term>Computer algebra system</term><term>Computer algebra system maple</term><term>Computer science</term><term>Concept formation steps</term><term>Congruence class</term><term>Congruence classes</term><term>Control rule</term><term>Control rules</term><term>Deduction volume</term><term>Discriminant</term><term>Discriminants</term><term>Equational reasoning</term><term>Equational reasoning strategy</term><term>Example construction</term><term>Exhaustive case analysis</term><term>External systems</term><term>Formal proof</term><term>Guide proof planning</term><term>Idempotent element</term><term>Inductive logic programming</term><term>International conference</term><term>Invariant property</term><term>Isomorphic</term><term>Isomorphism</term><term>Magma</term><term>Mathematical domain</term><term>Meier</term><term>Method calltrampm</term><term>Model generation</term><term>Model generator</term><term>More detail</term><term>Multi</term><term>Multiplication table</term><term>Multiplication tables</term><term>Nding discriminants</term><term>Open goal</term><term>Other hand</term><term>Other structure</term><term>Overall proof</term><term>Pages morgan kaufmann</term><term>Pages springer verlag</term><term>Planner</term><term>Planning process</term><term>Possible functions</term><term>Possible properties</term><term>Problem domain</term><term>Production rule</term><term>Production rules</term><term>Proof assumptions</term><term>Proof attempt</term><term>Proof plan</term><term>Proof planner</term><term>Proof planner multi</term><term>Proof planning</term><term>Proof plans</term><term>Proof procedure</term><term>Proof steps</term><term>Proof technique</term><term>Proof techniques</term><term>Provers</term><term>Quasigroups</term><term>Residue class</term><term>Residue class domain</term><term>Residue class sets</term><term>Residue class structure</term><term>Residue class structures</term><term>Residue classes</term><term>Right identity</term><term>Search space</term><term>Set1</term><term>Set2</term><term>Single element</term><term>Sorge</term><term>Springer verlag</term><term>Subsequent proof planning process</term><term>Suitable concepts</term><term>Suitable discriminant</term><term>Theorem provers</term><term>Theory formation</term><term>Theory formation system</term><term>Tramp</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>Royaume-Uni</li></country><region><li>Angleterre</li><li>Midlands de l'Ouest</li><li>Écosse</li></region><settlement><li>Birmingham</li><li>Édimbourg</li></settlement><orgName><li>Université d'Édimbourg</li><li>Université de Birmingham</li></orgName></list><tree><country name="Allemagne"><noRegion><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name></noRegion><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name></country><country name="Royaume-Uni"><region name="Angleterre"><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name></region><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Sarre/explor/MusicSarreV3/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000C09 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000C09 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Sarre
|area= MusicSarreV3
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:FFD345C780A55424D028DF36D3FA774C524D5F53
|texte= Employing Theory Formation to Guide Proof Planning
}}
| This area was generated with Dilib version V0.6.33. |  |